E,X1,X2:Type, info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), pred?:(E(?E)), e,e':E.
e < e'  prop{i:l} 

latex

Definitions	e < e', rel_plus(T; R), pred!(e;e'), x:A. B(x), Unit, Id, IdLnk, t  T
Lemmas	IdLnk wf, Id wf, unit wf, pred! wf, rel plus wf